\begin{tabbing}
dsm(${\it es}$;${\it ASM}$;$I$;$O$;$R$;$V$;$H$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=h{-}ordered(${\it es}$;$e$.$\uparrow$isl($I$($e$));$H$)\+
\\[0ex]c$\wedge$ \=(($\forall$$e$:\{$e$:E$\mid$ $\uparrow$isl($O$($e$))\} . ($R$($e$) $<$ $e$))\+
\\[0ex]\& ($\forall$$e$:\{$e$:E$\mid$ $\uparrow$isl($O$($e$))\} . outl($O$($e$)) = ${\it ASM}$(map($\lambda$${\it e'}$.outl($I$(${\it e'}$));$H$($R$($e$))))))
\-\-
\end{tabbing}